unsolvable $M$.pre($a$,$s$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(IdDeq; (($M$.2.2.2).1); $a$; $a$,$P$.($\neg$($\uparrow$($P$($s$)))))